home *** CD-ROM | disk | FTP | other *** search
/ PC-Blue - MS DOS Public Domain Library / PC-Blue MS-DOS Public Domain Library - NYACC.iso / vol350 / prolog.arc / LOGIC.ARC / SKOLEM.DOC < prev    next >
Encoding:
Text File  |  1986-11-07  |  1013 b   |  26 lines
  1. Contributed by Jim Adams of Bendix Aerospace.
  2.  
  3. The files "SKOLEM.OPS" and "SKOLEM.PRO" implement the translate 
  4. program described in C&M Appendix B and discussed in Chapter 10.  
  5. This is the program that translates predicate calculus statements 
  6. into Prolog statements.  The program is named SKOLEM.PRO and is 
  7. started on the command line with "pdprolog SKOLEM.OPS".  To 
  8. translate a predicate calculus statement you type, e.g. Three 
  9. sample predicate calculus statements are included in "SKOLEM.OPS" 
  10. and may be commented out.
  11.  
  12.  
  13.      ?- translate(all(X,s(X)<->exists(Y,e(X,Y)))).
  14. The answer should be something like:
  15.      s(X_1) :- e(X_1,Y_10).
  16.      e(X_1,f1(X_1) :- s(X_1).
  17. (The particular example comes from "x is a set iff there is a y
  18. such that x is an element of y", the first axiom of set theory.)
  19. The op codes are found in trans.ops and follow C&M:
  20.              <->   if and only if
  21.               ->   implies
  22.               &    and
  23.               #    or
  24.               ~    not
  25.  
  26.